/*
 * Auteurs : 	Bourgeois Jean-Louis	( jeanlouis.bourgeois@gmail.com )
 *		Ciabaud Yoann		( y.ciabaud@gmail.com )
 *
 * Date : Le 15-02-2007
 *
 * Dans ce fichier, sont regroupees les primitives necessaires a
 * l'interpretation d'une formule de cardinalite, par application 
 * de la methode DPC, ainsi que que l'algorithme DPC.
 *
 */
#ifndef DPC_H
#define DPC_H

#include "structure.h"


/**
 * Objectif :  choisir un litteral dans le cas d'un branchement
 * @param	*F	Notre Formule
 * @return	Le Litteral Choisi
 */
int heuristiqueLitteral( Formule *F );




/**
 * Objectif :  verifier si on fini de travailler sur la formule <i>F</i>
 * @param	*F	Formule considerre
 * @return		VRAI si termine, FAUX sinon.
 */
int estTermine( Formule *F );






/**
 * Objectif : remonter dans l'arborescence, en effancant l'affectation
 * 	de la variable <i>variable</i> dans la formule <i>F</i>
 * @param	*F		Formule etudiee
 * @param	litteral	Variable Liberee
 */
void libereVariable( Formule *F, int litteral);







/**
 * Objectif : 	Affecter la valeur <i>valeur</i> au litteral </i>litteral</l>
 *		dans la formule <i>F</i>
 * @param	*F		Formule etudiee
 * @param	litteral	litteral affecte
 * @param	valeur		nouvelle valeur de l
 * @return	VRAI		on peut affecter un litteral
 *		INCONSISTANT	modele inconsistant
 */
int affecteLitteral( Formule *F, int litteral, int valeur );





/**
 * Objectif : Recherche et affecte la premiere clause mono-litterale rencontree.
 * @param	*F		la formule etudiee
 * @param	*litteral	Pour recuperer la variable affectee
 * @return	VRAI		on peut affecter un mono-litteral
 *		FAUX		aucun mono-litteral
 *		INCONSISTANT	un mono-litteral existe, mais modele inconsistant
 */
int affecteMonoLitteraux( Formule *F, int *litteral );





/**
 * Objectif : Recherche un litteral pur et tente une affectation
 * @param	*F		La formule etudiee
 * @param	*litteral	Pour recuperer la variable affectee
 * @return	VRAI 		si un litteral est trouve et une affectation possible.
 *		FAUX 		si aucun litteral pur n'existe.
 *		INCONSISTANT	si un litteral est trouve mais pas une affectation.
 */
int affecteLitterauxPurs( Formule *F, int *litteral );






/**
 * Objectif : tester si la formule <i>F<i/> est consistante
 * @param	*F		Formule a tester
 * @return	CONSISTANT	si la formule est satisfiable
 *		INCONSISTANT	sinon
 */
int dpc( Formule *F );

/**
 * Objectif : tester si la formule <i>F<i/> est consistante
 * @param	*F		Formule a tester
 * @return	CONSISTANT	si la formule est satisfiable
 *		INCONSISTANT	sinon
 */
int dpcIteratif( Formule *F );





#endif

